If the goal is to produce human friendly error messages, why are these tools not using the message field? I would say we should probably not add back name but figure out why is message not used.

If the goal is to produce human friendly error messages, why are these tools not using the message field? I would say we should probably not add back name but figure out why is message not used.

SystemVerilog assertions do not have messages in the first place; relying on messages thus limits us to yosys-based tooling

on the other hand, the example given in the RFC could definitely be fixed on sby side

SystemVerilog assertions do not have messages in the first place; relying on messages thus limits us to yosys-based tooling

From my memory of talking to Jannis, they sort of do, in that assert x else $error is treated specially, or something along those lines. This is also how the Yosys $check cell is implemented, and both parsing and emitting should respect that.

I care more about Jasper than sby at the moment to be honest.
Jasper names the properties at elaboration time and $error can include formatting, so I guess that is why its not used?

@jix, would you happen to have advice here? I've never used Jasper.

We have discussed this RFC on the 2025-05-26 core subsystem meeting. The disposition was to postpone.

The motivation in the RFC (sby needs it to print a good message) was deemed insufficient, as we already have messages attached to properties. Likewise for the secondary motivation of using Jasper — if a workaround is needed, we can just generate labels from messages in some part of the stack.

More importantly, Amaranth currently doesn't have well-defined formal semantics — there is no formal verification mode in Amaranth at all, and all formal-specific language features are essentially RTLIL legacy with no clear definition other than "what yosys and sby do". Any kind of RFC proposing features with FV justification thus has to be blocked by necessity until a formal model is proposed.